from z3 import *

S = DeclareSort("S")
a, b, c, d, e, s, t = Consts("a b c d e s t", S)
f = Function("f", S, S, S)
g = Function("g", S, S)
solve([a == b, b == c, d == e, b == s, d == t, f(a, g(d)) != f(g(e), b)])

# 生成模型如下:
# > [c = S!val!0,
# > e = S!val!1,
# > t = S!val!1,
# > s = S!val!0,
# > d = S!val!1,
# > a = S!val!0,
# > b = S!val!0,
# > f = [(S!val!2, S!val!0) -> S!val!4, else -> S!val!3],
# > g = [else -> S!val!2]
